i:Id, R:Realizer.
Rplus?(R)  Rnone?(R)  R-da(R;i) = if R-loc(R) = i Rda(R) else  fi  x:Knd fp Type 

latex

Definitions

Realizer, rec(x.A(x)), DeclaredType(ds;x), State(ds), IdLnk, type List, es realizer ind Rnone compseq tag def, es realizer ind Rplus compseq tag def, Rplus?(x1), Rnone?(x1), True, a:A fp B(a), False, es realizer ind Rinit compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rbframe compseq tag def, R-da(R;i), R-loc(R), Rda(R), es realizer ind Rrframe compseq tag def, left+right, Unit, P  Q, P & Q, x:AB(x), P  Q, x:AB(x), f  g, lnk-decl(l;dt), KindDeq, source(l), x : v, locl(a), a = b, , b, A, b, Prop, s = t, Id, , x:A. B(x), x. t(x), x.A(x), Type, t  T, Knd

Lemmas

Knd wf, fpf-empty wf, Id wf, assert wf, not wf, bnot wf, bool wf, eq id wf, locl wf, fpf-single wf, lsrc wf, Kind-deq wf, lnk-decl wf, fpf-join wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, false wf, true wf, IdLnk wf, decl-state wf, fpf wf, decl-type wf, unit wf, es realizer wf